<!DOCTYPE html>
<!--
     SPDX-License-Identifier: CC-BY-SA-4.0
     SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
-->
<!-- Page last generated 2025-02-20 03:16:15 +0000 -->
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>CAmkES timer tutorial | seL4 docs</title>

    <!-- Our stylesheet and theme stylesheet.  Contains bootstrap. -->
    <link rel="stylesheet" href="/assets/css/style.css" type="text/css">
    <!-- Font awesome -->
    <link href="https://use.fontawesome.com/releases/v5.0.8/css/all.css" rel="stylesheet">
    <link href="https://fonts.googleapis.com/css2?family=Roboto&display=swap" rel="stylesheet">
    <!-- Pygments syntax highlighting  -->
    <link rel="stylesheet" href="/assets/css/highlighting/trac.css" type="text/css">
    <link rel="icon" type="image/x-icon" href="/assets/favicon.ico"><script defer data-domain="docs.sel4.systems"
	    src="https://analytics.sel4.systems/js/script.js"></script></head>

  <body class="container-fluid">

    



<header>
  <ul class="row menu">
    <li class="col-xs-12 col-md-2" >
            <a href="https://sel4.systems" class="skip-icon">
              <img class="img-responsive" src="/assets/logo-text-white.svg" alt="seL4 logo" />
            </a>
    </li>
    <li class="col-xs-12 col-md-10 menu">
      <nav aria-label="Banner links">
        <h2><a href="/Resources" />Resources</h2>
        <h2><a href="/processes" />Contributing</a></h2>
        <h2><a href="/projects" />Projects</h2>
        <h2><a href="/Tutorials" />Tutorials</h2>
        <iframe title="DuckDuckGo search bar" src="https://duckduckgo.com/search.html?site=docs.sel4.systems&prefill=Search%20sel4.systems" style="overflow:hidden;margin-bottom:10px; padding:0;height:40px;float:right;border-width: 0px"></iframe>
      </nav>
    </li>
  </ul>
  <div class="clear"></div>
  
<div class="breadcrumbs bootstrap hidden-sm-down">
  <nav class="sel-breadcrumb" aria-label="Breadcrumb" >
    <ol class=" list-unstyled" vocab="http://schema.org/" typeof="BreadcrumbList">
      
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/">
              <span property="name"><b>seL4 Docs</b></span>
            </a>
            <meta property="position" content="1" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/Tutorials/">
              <span property="name"><b>Tutorials</b></span>
            </a>
            <meta property="position" content="2" />
        </li>
      
        

        
          <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <span property="name">CAmkES timer tutorial</span>
            <meta property="position" content="3" /></li>
          
    </ol>
  </nav>
  <nav class="sel-version" aria-label="Current Versions">
    <ol class="list-unstyled">
      <li class="list-unstyled text-right" style="margin-left:auto; padding:0rem 0rem;">
        Current versions:</li>
      <li class="list-unstyled text-right">
      <a href="/releases/sel4/13.0.0"><b>seL4-13.0.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/microkit/1.4.1"><b>microkit-1.4.1</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/camkes/camkes-3.11.0"><b>camkes-3.11.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/capdl/0.3.0"><b>capDL-0.3.0</b></a></li>
      </ol>
  </nav>
  <div class='clear'></div>
</div>


</header>

    <main>
      <div class="row">
  <div class="hidden-xs col-sm-4 col-md-3 col-lg-2">
    

<div class="sidebar">
  <ul class="nav nav-sidebar tutorial-sidebar">
    <li class="nav-section">Getting started</li>
      <li><a href="/Tutorials/">Overview</a></li>
      <li><a href="/Tutorials/pathways">Tutorial pathways</a></li>
    <li class="nav-section">seL4</li>
      <li><a href="/Tutorials/setting-up">Setting up your machine</a></li>
      <li><a href="/Tutorials/get-the-tutorials">Getting the tutorials</a></li>
      <li><a href="/Tutorials/hello-world">Hello world</a></li>
      <li><a href="/Tutorials/capabilities">Capabilities</a></li>
      <li><a href="/Tutorials/untyped">Untyped</a></li>
      <li><a href="/Tutorials/mapping">Mapping</a></li>
      <li><a href="/Tutorials/threads">Threads</a></li>
      <li><a href="/Tutorials/ipc">IPC</a></li>
      <li><a href="/Tutorials/notifications">Notifications</a></li>
      <li><a href="/Tutorials/interrupts">Interrupts</a></li>
      <li><a href="/Tutorials/fault-handlers">Fault handling</a></li>
      <li><a href="/Tutorials/mcs">MCS extensions</a></li>
    <li class="nav-section">C Libraries</li>
      <li><a href="/Tutorials/libraries-1">Initialisation &amp; threading</a></li>
      <li><a href="/Tutorials/libraries-2">IPC</a></li>
      <li><a href="/Tutorials/libraries-3">Processes &amp; Elf loading</a></li>
      <li><a href="/Tutorials/libraries-4">Timer</a></li>
    <li class="nav-section">Microkit</li>
      <li><a href="https://trustworthy.systems/projects/microkit/tutorial/">Tutorial</a></li>
    <li class="nav-section">CAmkES</li>
      <li><a href="/Tutorials/hello-camkes-0">Hello CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-1">Introduction to CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-2">Events in CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-timer">CAmkES timer tutorial</a></li>
      <li><a href="/Tutorials/camkes-vm-linux">CAmkES VM</a></li>
      <li><a href="/Tutorials/camkes-vm-crossvm">CAmkES cross-VM connectors</a></li>
    <li class="nav-section">Rust</li>
      <li><a href="https://github.com/seL4/rust-sel4">GitHub</a></li>
    <li class="nav-section">Resources</li>
      <li><a href="https://sel4.systems/Info/Docs/seL4-manual-latest.pdf">seL4 Manual</a></li>
      <li><a href="/projects/sel4/api-doc.html">seL4 API reference</a></li>
      <li><a href="/Tutorials/how-to">How to: a quick solutions guide</a></li>
      <li><a href="/projects/sel4-tutorials/debugging-guide">Debugging guide</a></li>
      <li><a href="/Resources#contact">Help contacts</a></li>
  </ul>
</div>

  </div>
  <div class="content col-sm-8 col-md-6 col-lg-7 main">

    
<!--
  Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)

  SPDX-License-Identifier: BSD-2-Clause
-->

<h1 id="camkes-timer-tutorial">CAmkES Timer Tutorial</h1>

<p>This tutorial guides you through setting up a sample timer driver component in
CAmkES and using it to delay for 2 seconds. For this tutorial, we will be using
the ZYNQ7000 ARM-based platform. This platform can be simulated via QEMU so it
is not a problem if you do not have access to the actual physical board.</p>

<p>The tutorial also has two parts to it. The first part will teach you how to
manually define hardware details to configure the hardware component and
initialise hardware resources.  The second part will teach you how to use a
CAmkES connector to initialise hardware resources automatically for you.</p>

<p>The solutions to this tutorial primarily uses the method of manually defining
hardware details. The solutions to the second part are also included, albeit
commented out.</p>

<h2 id="initialising">Initialising</h2>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="c"># For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials</span>
<span class="c">#</span>
<span class="c"># Follow these instructions to initialise the tutorial</span>
<span class="c"># initialising the build directory with a tutorial exercise</span>
./init <span class="nt">--tut</span> hello-camkes-timer
<span class="c"># building the tutorial exercise</span>
<span class="nb">cd </span>hello-camkes-timer_build
ninja
</code></pre></div></div>

<h2 id="prerequisites">Prerequisites</h2>

<ol>
  <li><a href="https://docs.sel4.systems/HostDependencies">Set up your machine</a>.</li>
  <li><a href="/Tutorials/hello-camkes-2">Camkes 2</a></li>
</ol>

<h2 id="capdl-loader">CapDL Loader</h2>

<p>This tutorial uses the <em>capDL loader</em>, a root task which allocates statically
 configured objects and capabilities.</p>

<details>
  <summary>Get CapDL</summary>
  <p>The capDL loader parses
a static description of the system and the relevant ELF binaries.
It is primarily used in <a href="https://docs.sel4.systems/CAmkES/">Camkes</a> projects
but we also use it in the tutorials to reduce redundant code.
The program that you construct will end up with its own CSpace and VSpace, which are separate
from the root task, meaning CSlots like <code class="language-plaintext highlighter-rouge">seL4_CapInitThreadVSpace</code> have no meaning
in applications loaded by the capDL loader.
<br />
More information about CapDL projects can be found <a href="https://docs.sel4.systems/CapDL.html">here</a>.
<br />
For this tutorial clone the <a href="https://github.com/sel4/capdl">CapDL repo</a>. This can be added in a directory that is adjacent to the tutorials-manifest directory.</p>
</details>

<h2 id="initialising-1">Initialising</h2>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="c"># For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials</span>
<span class="c">#</span>
<span class="c"># Follow these instructions to initialise the tutorial</span>
<span class="c"># initialising the build directory with a tutorial exercise</span>
./init <span class="nt">--tut</span> hello-camkes-timer
<span class="c"># building the tutorial exercise</span>
<span class="nb">cd </span>hello-camkes-timer_build
ninja
</code></pre></div></div>

<details>
  <summary><em>Hint:</em> tutorial solutions</summary>
  <p><br />
All tutorials come with complete solutions. To get solutions run:</p>

  <div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="c"># For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials</span>
<span class="c">#</span>
<span class="c"># Follow these instructions to initialise the tutorial</span>
<span class="c"># initialising the build directory with a tutorial exercise</span>
./init <span class="nt">--solution</span> <span class="nt">--tut</span> hello-camkes-timer
<span class="c"># building the tutorial exercise</span>
<span class="nb">cd </span>hello-camkes-timer_build
ninja
</code></pre></div>  </div>

</details>

<h2 id="exercises---part-1">Exercises - Part 1</h2>

<h3 id="instantiate-a-timer-and-timerbase">Instantiate a Timer and Timerbase</h3>
<p>Start in <code class="language-plaintext highlighter-rouge">hello-camkes-timer.camkes</code>.</p>

<p>Instantiate some components. You’re already given one component instance</p>
<ul>
  <li><code class="language-plaintext highlighter-rouge">client</code>. You need to instantiate additional components, a timer driver and
a component instance representing the timer hardware itself. Look
in <code class="language-plaintext highlighter-rouge">components/Timer/Timer.camkes</code> for the definitions of the components.</li>
</ul>

<p>Once you open the file, you will notice three different components. The <code class="language-plaintext highlighter-rouge">Timer</code>
and <code class="language-plaintext highlighter-rouge">Timerbase</code> components represents the timer driver and the timer hardware
respectively. The <code class="language-plaintext highlighter-rouge">TimerDTB</code> component represents both the timer driver and the
timer hardware. This component is meant to be used with the <code class="language-plaintext highlighter-rouge">seL4DTBHardware</code>
CAmkES connector to automatically initialise hardware resources. The second
part of the tutorial will go into more detail about the <code class="language-plaintext highlighter-rouge">TimerDTB</code> component
and the <code class="language-plaintext highlighter-rouge">seL4DTBHardware</code> connector.</p>

<p>For now, instantiate the <code class="language-plaintext highlighter-rouge">Timer</code> and <code class="language-plaintext highlighter-rouge">Timerbase</code> components.</p>

<p>Note the lines <code class="language-plaintext highlighter-rouge">connection seL4RPCCall hello_timer(from client.hello, to
timer.hello);</code> and <code class="language-plaintext highlighter-rouge">timer.sem_value = 0;</code> in the <code class="language-plaintext highlighter-rouge">hello-camkes-timer.camkes</code>
file. They assume that the name of the timer ‘‘driver’’ will be <code class="language-plaintext highlighter-rouge">timer</code>. If you
wish to call your driver something else, you’ll have to change these lines.</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    /* Part 1, TASK 1: component instances */
    /* hint 1: one hardware component and one driver component
        * hint 2: look at
        * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
        */
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    /* Part 1, TASK 1: component instances */
    component Timerbase timerbase;
    component Timer timer;
</code></pre></div>  </div>
</details>

<h3 id="connect-a-timer-driver-component">Connect a timer driver component</h3>
<p>Connect the timer driver component (<code class="language-plaintext highlighter-rouge">Timer</code>) to the timer hardware component
(<code class="language-plaintext highlighter-rouge">Timerbase</code>). The timer hardware component exposes two interfaces which must
be connected to the timer driver. One of these represents memory-mapped
registers. The other represents an interrupt.</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    /* Part 1, TASK 2: connections */
    /* hint 1: use seL4HardwareMMIO to connect device memory
        * hint 2: use seL4HardwareInterrupt to connect interrupt
        * hint 3: look at
        * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
        */
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    /* Part 1, TASK 2: connections */
    connection seL4HardwareMMIO timer_mem(from timer.reg, to timerbase.reg);
    connection seL4HardwareInterrupt timer_irq(from timerbase.irq, to timer.irq);
</code></pre></div>  </div>
</details>

<h3 id="configure-a-timer-hardware-component-instance">Configure a timer hardware component instance</h3>
<p>Configure the timer hardware component instance with device-specific info. The
physical address of the timer’s memory-mapped registers, and its IRQ number
must both be configured.</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    /* Part 1, TASK 3: hardware resources */
    /* Timer and Timerbase:
        * hint 1: find out the device memory address and IRQ number from the hardware data sheet
        * hint 2: look at
        * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#hardware-components
        */
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    /* Part 1, TASK 3: hardware resources */
    timerbase.reg_paddr = 0xF8001000;   // paddr of mmio registers
    timerbase.reg_size = 0x1000;        // size of mmio registers
    timerbase.irq_irq_number = 42;      // timer irq number
</code></pre></div>  </div>
</details>

<h3 id="call-into-a-supplied-driver-to-handle-the-interrupt">Call into a supplied driver to handle the interrupt</h3>
<p>Now open <code class="language-plaintext highlighter-rouge">components/Timer/src/timer.c</code>.</p>

<p>We’ll start by completing the <code class="language-plaintext highlighter-rouge">irq_handle</code> function, which is called in
response to each timer interrupt. Note the name of this function. It follows
the naming convention <code class="language-plaintext highlighter-rouge">&lt;interface&gt;_handle</code>, where <code class="language-plaintext highlighter-rouge">&lt;interface&gt;</code> is the name of
an IRQ interface connected with <code class="language-plaintext highlighter-rouge">seL4HardwareInterrupt</code>. When an interrupt is
received on the interface <code class="language-plaintext highlighter-rouge">&lt;interface&gt;</code>, the function <code class="language-plaintext highlighter-rouge">&lt;interface&gt;_handle</code> will
be called.</p>

<p>The implementation of the timer driver is located inside a different folder and
can be found in the <code class="language-plaintext highlighter-rouge">projects/sel4-tutorials/zynq_timer_driver</code> folder from the
root of the projects directory, i.e. where the <code class="language-plaintext highlighter-rouge">.repo</code> folder can be found and
where the initial <code class="language-plaintext highlighter-rouge">repo init</code> command was executed.</p>

<p>This task is to call the <code class="language-plaintext highlighter-rouge">timer_handle_irq</code> function from the supply driver to
inform the driver that an interrupt has occurred.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* Part 1, TASK 4: call into the supplied driver to handle the interrupt. */</span>
    <span class="cm">/* hint: timer_handle_irq
     */</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* Part 1, TASK 4: call into the supplied driver to handle the interrupt. */</span>
    <span class="n">timer_handle_irq</span><span class="p">(</span><span class="o">&amp;</span><span class="n">timer_drv</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<h3 id="stop-a-timer">Stop a timer</h3>
<p>Stop the timer from running. The <code class="language-plaintext highlighter-rouge">timer_stop</code> function will be helpful here.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* Part 1, TASK 5: stop the timer. */</span>
    <span class="cm">/* hint: timer_stop
     */</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* Part 1, TASK 5: stop the timer. */</span>
    <span class="n">timer_stop</span><span class="p">(</span><span class="o">&amp;</span><span class="n">timer_drv</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<h3 id="acknowledge-an-interrupt">Acknowledge an interrupt</h3>
<p>The interrupt now needs to be acknowledged.</p>

<p>CAmkES generates the seL4-specific code for ack-ing an interrupt and provides a
function <code class="language-plaintext highlighter-rouge">&lt;interface&gt;_acknowldege</code> for IRQ interfaces (specifically those
connected with <code class="language-plaintext highlighter-rouge">seL4HardwareInterrupt</code>).</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* Part 1, TASK 6: acknowledge the interrupt */</span>
    <span class="cm">/* hint 1: use the function &lt;irq interface name&gt;_acknowledge()
     */</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* Part 1, TASK 6: acknowledge the interrupt */</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">irq_acknowledge</span><span class="p">();</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span> <span class="o">!=</span> <span class="mi">0</span><span class="p">,</span> <span class="s">"failed to acknowledge interrupt"</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<h3 id="get-a-timer-handler">Get a timer handler</h3>
<p>Now we’ll complete <code class="language-plaintext highlighter-rouge">hello__init</code> - a function which is called once
before the component’s interfaces start running.</p>

<p>We need to initialise a handle to the timer driver for this device, and store a
handle to the driver in the global variable <code class="language-plaintext highlighter-rouge">timer_drv</code>.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* Part 1, TASK 7: call into the supplied driver to get the timer handler */</span>
    <span class="cm">/* hint1: timer_init
     * hint2: The timer ID is supplied as a #define in this file
     * hint3: The register's variable name is the same name as the dataport in the Timer component
     */</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* Part 1, TASK 7: call into the supplied driver to get the timer handler */</span>
    <span class="kt">int</span> <span class="n">error</span> <span class="o">=</span> <span class="n">timer_init</span><span class="p">(</span><span class="o">&amp;</span><span class="n">timer_drv</span><span class="p">,</span> <span class="n">DEFAULT_TIMER_ID</span><span class="p">,</span> <span class="n">reg</span><span class="p">);</span>
    <span class="n">assert</span><span class="p">(</span><span class="n">error</span> <span class="o">==</span> <span class="mi">0</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<h3 id="start-a-timer">Start a timer</h3>
<p>After initialising the timer, we now need to start the timer. Do so by calling
<code class="language-plaintext highlighter-rouge">timer_start</code> and passing the handle to the driver.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* Part 1, TASK 8: start the timer */</span>
    <span class="cm">/* hint: timer_start
     */</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* Part 1, TASK 8: start the timer */</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">timer_start</span><span class="p">(</span><span class="o">&amp;</span><span class="n">timer_drv</span><span class="p">);</span>
    <span class="n">assert</span><span class="p">(</span><span class="n">error</span> <span class="o">==</span> <span class="mi">0</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<h3 id="implement-a-rpc-interface">Implement a RPC interface</h3>
<p>Note that this task is to understand the existing code. You won’t have
to modify anything for this task.</p>

<p>Implement the <code class="language-plaintext highlighter-rouge">timer_inf</code> RPC interface. This interface is defined in
<code class="language-plaintext highlighter-rouge">interfaces/timer.camkes</code>, and contains a single method, <code class="language-plaintext highlighter-rouge">sleep</code>, which
should return after a given number of seconds. in
<code class="language-plaintext highlighter-rouge">components/Timer/Timer.camkes</code>, we can see that the <code class="language-plaintext highlighter-rouge">timer_inf</code> interface
exposed by the <code class="language-plaintext highlighter-rouge">Timer</code> component is called <code class="language-plaintext highlighter-rouge">hello</code>. Thus, the function we
need to implement is called <code class="language-plaintext highlighter-rouge">hello_sleep</code>.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* Part 1, TASK 9: implement the rpc function. */</span>
    <span class="cm">/* hint 1: the name of the function to implement is a composition of an interface name and a function name:
    * i.e.: &lt;interface&gt;_&lt;function&gt;
    * hint 2: the interfaces available are defined by the component, e.g. in components/timer/timer.camkes
    * hint 3: the function name is defined by the interface definition, e.g. in interfaces/timer.camkes
    * hint 4: so the function would be: hello_sleep()
    * hint 5: the camkes 'int' type maps to 'int' in c
    * hint 6: invoke a function in supplied driver the to set up the timer
    * hint 7: look at https://github.com/sel4/camkes-tool/blob/master/docs/index.md#creating-an-application
    */</span>
</code></pre></div></div>
<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="cm">/* Part 1, TASK 9: implement the rpc function. */</span>
<span class="kt">void</span> <span class="nf">hello_sleep</span><span class="p">(</span><span class="kt">int</span> <span class="n">sec</span><span class="p">)</span> <span class="p">{</span>
    <span class="kt">int</span> <span class="n">error</span> <span class="o">=</span> <span class="mi">0</span><span class="p">;</span>
</code></pre></div>  </div>
</details>

<h3 id="set-a-timer-interrupt">Set a timer interrupt</h3>
<p>Tell the timer to interrupt after the given number of seconds. The
<code class="language-plaintext highlighter-rouge">timer_set_timeout</code> function from the included driver will help. Note that it
expects its time argument to be given in nanoseconds.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* Part 1, TASK 10: invoke a function in the supplied driver to set a timeout */</span>
    <span class="cm">/* hint1: timer_set_timeout
     * hint2: periodic should be set to false
     */</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* Part 1, TASK 10: invoke a function in the supplied driver to set a timeout */</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">timer_set_timeout</span><span class="p">(</span><span class="o">&amp;</span><span class="n">timer_drv</span><span class="p">,</span> <span class="n">sec</span> <span class="o">*</span> <span class="n">NS_IN_SECOND</span><span class="p">,</span> <span class="nb">false</span><span class="p">);</span>
    <span class="n">assert</span><span class="p">(</span><span class="n">error</span> <span class="o">==</span> <span class="mi">0</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>Note the existing code in <code class="language-plaintext highlighter-rouge">hello_sleep</code>. It waits on a binary semaphore.
<code class="language-plaintext highlighter-rouge">irq_handle</code> will be called on another thread when the timer interrupt occurs,
and that function will post to the binary semaphore, unblocking us and allowing
the function to return after the delay.</p>

<p>Expect the following output with a 2 second delay between the last 2
lines:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Starting the client
------Sleep for 2 seconds------
After the client: wakeup
</code></pre></div></div>

<h2 id="exercises---part-2">Exercises - Part 2</h2>

<p>Now that you’ve learnt how to manually define the hardware details of a
hardware component to initialise hardware resources, this part of the tutorial
will teach you how to use the <code class="language-plaintext highlighter-rouge">seL4DTBHardware</code> connector to do that
automatically.</p>

<p>The connector requires a devicetree blob which describes an ARM platform.
Additionally, the blob’s interrupt fields also need to follow the same format
of the ARM GIC v1 and v2. There are devicetree source files bundled with the
kernel, look in the <code class="language-plaintext highlighter-rouge">tools/dts/</code> folder of the kernel sources. If a suitable
devicetree blob is not available for your platform, then do not proceed with
the tutorial.</p>

<h3 id="instantiate-a-timerdtb-component">Instantiate a TimerDTB component</h3>
<p>Navigate to the <code class="language-plaintext highlighter-rouge">hello-camkes-timer.camkes</code> file.</p>

<p>Remove the <code class="language-plaintext highlighter-rouge">Timerbase</code> and <code class="language-plaintext highlighter-rouge">Timer</code> component instantiations and instantiate a
<code class="language-plaintext highlighter-rouge">TimerDTB</code> component instead. Also change the <code class="language-plaintext highlighter-rouge">connection seL4RPCCall
hello_timer(from client.hello, to timer.hello);</code> and <code class="language-plaintext highlighter-rouge">timer.sem_value = 0;</code>
lines if necessary.</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    /* Part 2, TASK 1: component instances */
    /* hint 1: a single TimerDTB component
    * hint 2: look at
    * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
    */
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    /* Part 2, TASK 1: component instances */
    //uncomment the line below
//    component TimerDTB timer;
</code></pre></div>  </div>
</details>

<h3 id="connect-interfaces-using-the-sel4dtbhardware-connector">Connect interfaces using the seL4DTBHardware connector</h3>
<p>Remove the <code class="language-plaintext highlighter-rouge">seL4HardwareMMIO</code> and <code class="language-plaintext highlighter-rouge">seL4HardwareInterrupt</code> connections. Connect
the two interfaces inside the <code class="language-plaintext highlighter-rouge">TimerDTB</code> component with the <code class="language-plaintext highlighter-rouge">seL4DTBHardware</code>
connector.</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    /* Part 2, TASK 2: connections */
    /* hint 1: connect the dummy_source and timer interfaces
    * hint 2: the dummy_source should be the 'from' end
    * hint 3: look at
    * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
    */
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>      /* Part 2, TASK 2: connections */
      // uncomment the line below
//    connection seL4DTBHardware timer_dtb(from timer.dummy_source, to timer.tmr);
</code></pre></div>  </div>
</details>

<h3 id="configure-the-timerdtb-component">Configure the TimerDTB component</h3>
<p>Before opening <code class="language-plaintext highlighter-rouge">components/Timer/Timer.camkes</code>, remove the <code class="language-plaintext highlighter-rouge">Timerbase</code> settings
inside the configurations block.</p>

<p>Configure the <code class="language-plaintext highlighter-rouge">TimerDTB</code> component to pass in the correct DTB path to a timer
to the connector and also initialise the interrupt resources for the timer.
This will allow the connector to read a device node from the devicetree blob
and grab the necessary data to initialise hardware resources. More
specifically, it reads the registers field and optionally the interrupts field
to allocate memory and interrupts.</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    /* Part 2, TASK 3: hardware resources */
    /* TimerDTB:
     * hint 1: look in the DTB/DTS for the path of a timer
     * hint 2: set the 'dtb' setting for the tmr interface in the TimerDTB component,
     *         e.g. foo.dtb = dtb({"path" : "/bar"});
     * hint 3: set the 'generate_interrupts' setting to 1
     */
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>     /* Part 2, TASK 3: hardware resources */
     // uncomment the lines below
//    tmr.dtb = dtb({"path" : "/amba/timer@f8001000"});   // path of the timer in the DTB
//    tmr.generate_interrupts = 1;                        // tell seL4DTBHardware to init interrupts
</code></pre></div>  </div>
</details>

<h3 id="handle-the-interrupt">Handle the interrupt</h3>
<p>Move to <code class="language-plaintext highlighter-rouge">components/TimerDTB/src/timerdtb.c</code>.</p>

<p>Similar to part one, we’ll start with the <code class="language-plaintext highlighter-rouge">tmr_irq_handle</code> function. This
function is called in response to a timer interrupt. The name of the function
has a special meaning and the meaning is unique to the <code class="language-plaintext highlighter-rouge">seL4DTBHardware</code>
connector.</p>

<p>The IRQ handling functions of the connector follows the naming convention
<code class="language-plaintext highlighter-rouge">&lt;to_interface&gt;_irq_handle</code>, where <code class="language-plaintext highlighter-rouge">&lt;to_interface&gt;</code> is the name of the
interface of the ‘to’ end in an instance of a <code class="language-plaintext highlighter-rouge">seL4DTBHardware</code> connection.
Also notice that it takes a <code class="language-plaintext highlighter-rouge">ps_irq_t *</code> type. This is because, for a given
device, there may be multiple interrupts associated with the device. A
<code class="language-plaintext highlighter-rouge">ps_irq_t</code> struct is given to the IRQ handling function and it contains
information about the interrupt, allowing the handler to differentiate between
the numerous interrupts of a device.</p>

<p>Likewise with part one, the implementation of the timer driver is in the
included driver in <code class="language-plaintext highlighter-rouge">timer_driver</code> and the task here is to call
<code class="language-plaintext highlighter-rouge">timer_handle_irq</code>.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* Part 2, TASK 4: call into the supplied driver to handle the interrupt. */</span>
    <span class="cm">/* hint: timer_handle_irq
     */</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* Part 2, TASK 4: call into the supplied driver to handle the interrupt. */</span>
    <span class="n">timer_handle_irq</span><span class="p">(</span><span class="o">&amp;</span><span class="n">timer_drv</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<h3 id="stop-a-timer-1">Stop a timer</h3>
<p>Stop the timer from running. The <code class="language-plaintext highlighter-rouge">timer_stop</code> function will be helpful here.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* Part 2, TASK 5: stop the timer. */</span>
    <span class="cm">/* hint: timer_stop
     */</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* Part 2, TASK 5: stop the timer. */</span>
    <span class="n">timer_stop</span><span class="p">(</span><span class="o">&amp;</span><span class="n">timer_drv</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<h3 id="acknowledge-the-interrupt">Acknowledge the interrupt</h3>
<p>Again, the interrupt now has to be acknowledged.</p>

<p>For the <code class="language-plaintext highlighter-rouge">seL4DTBHardware</code> connector, CAmkES also generates and provides a
function to acknowledge interrupts. This function follows a similar naming
convention to the IRQ handler above, <code class="language-plaintext highlighter-rouge">&lt;to_interface&gt;_irq_acknowledge</code> also
takes in a <code class="language-plaintext highlighter-rouge">ps_irq_t *</code> argument. Similarly, the <code class="language-plaintext highlighter-rouge">ps_irq_t *</code> argument helps
CAmkES to differentiate between the possibly many interrupts of a device that
you wish to acknowledge.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* Part 2, TASK 6: acknowledge the interrupt */</span>
    <span class="cm">/* hint 1: use the function &lt;to_interface_name&gt;_irq_acknowledge()
     * hint 2: pass in the 'irq' variable to the function
     */</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* Part 2, TASK 6: acknowledge the interrupt */</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">tmr_irq_acknowledge</span><span class="p">(</span><span class="n">irq</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span> <span class="o">!=</span> <span class="mi">0</span><span class="p">,</span> <span class="s">"failed to acknowledge interrupt"</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<h3 id="task-7---10">TASK 7 - 10</h3>

<p>Task 7 to 10 are the exact same as the tasks in part one.</p>

<p>You should also expect the same output as the first part.</p>



<p style="text-align: right;">

      Next: <a href="/Tutorials/camkes-vm-linux">CAmkES VM</a>
</p>

<hr>
    <p><em>Tutorial included from <a href="https://github.com/sel4/sel4-tutorials/blob/master/tutorials/hello-camkes-timer/hello-camkes-timer.md">github repo</a> <a href="https://github.com/sel4/sel4-tutorials/edit/master/tutorials/hello-camkes-timer/hello-camkes-timer.md">edit</a></em></p>
  </div>

  
    
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
    <ul id="toc" class="section-nav">
<li class="toc-entry toc-h2"><a href="#initialising">Initialising</a></li>
<li class="toc-entry toc-h2"><a href="#prerequisites">Prerequisites</a></li>
<li class="toc-entry toc-h2"><a href="#capdl-loader">CapDL Loader</a></li>
<li class="toc-entry toc-h2"><a href="#initialising-1">Initialising</a></li>
<li class="toc-entry toc-h2"><a href="#exercises---part-1">Exercises - Part 1</a>
<ul>
<li class="toc-entry toc-h3"><a href="#instantiate-a-timer-and-timerbase">Instantiate a Timer and Timerbase</a></li>
<li class="toc-entry toc-h3"><a href="#connect-a-timer-driver-component">Connect a timer driver component</a></li>
<li class="toc-entry toc-h3"><a href="#configure-a-timer-hardware-component-instance">Configure a timer hardware component instance</a></li>
<li class="toc-entry toc-h3"><a href="#call-into-a-supplied-driver-to-handle-the-interrupt">Call into a supplied driver to handle the interrupt</a></li>
<li class="toc-entry toc-h3"><a href="#stop-a-timer">Stop a timer</a></li>
<li class="toc-entry toc-h3"><a href="#acknowledge-an-interrupt">Acknowledge an interrupt</a></li>
<li class="toc-entry toc-h3"><a href="#get-a-timer-handler">Get a timer handler</a></li>
<li class="toc-entry toc-h3"><a href="#start-a-timer">Start a timer</a></li>
<li class="toc-entry toc-h3"><a href="#implement-a-rpc-interface">Implement a RPC interface</a></li>
<li class="toc-entry toc-h3"><a href="#set-a-timer-interrupt">Set a timer interrupt</a></li>
</ul>
</li>
<li class="toc-entry toc-h2"><a href="#exercises---part-2">Exercises - Part 2</a>
<ul>
<li class="toc-entry toc-h3"><a href="#instantiate-a-timerdtb-component">Instantiate a TimerDTB component</a></li>
<li class="toc-entry toc-h3"><a href="#connect-interfaces-using-the-sel4dtbhardware-connector">Connect interfaces using the seL4DTBHardware connector</a></li>
<li class="toc-entry toc-h3"><a href="#configure-the-timerdtb-component">Configure the TimerDTB component</a></li>
<li class="toc-entry toc-h3"><a href="#handle-the-interrupt">Handle the interrupt</a></li>
<li class="toc-entry toc-h3"><a href="#stop-a-timer-1">Stop a timer</a></li>
<li class="toc-entry toc-h3"><a href="#acknowledge-the-interrupt">Acknowledge the interrupt</a></li>
<li class="toc-entry toc-h3"><a href="#task-7---10">TASK 7 - 10</a></li>
</ul>
</li>
</ul>
</div>

  
</div>
<script src="/assets/js/toggle-markdown.js"></script>

    </main>
    


<footer class="site-footer">

  <h2 class="footer-heading">seL4 docs</h2>

  <div class="footer-col-wrapper">

    <div class="col-md-2">
      



<ul class="social-media-list">
  <li><a href="https://github.com/sel4"><i class="fab fa-github"></i> <span class="username">sel4</span></a></li><li><a href="https://github.com/sel4proj"><i class="fab fa-github"></i> <span class="username">sel4proj</span></a></li>
</ul>

    </div>

    <div class="col-md-8">
      <ul class="list-unstyled">
        <li>
          This site is for displaying seL4 related documentation.  Pull requests are welcome.
        </li>
        
          <li>
            Site last updated: Fri Feb 7 10:17:38 2025 +1100 ee78c8857c
          </li>
          <li>
                Page last updated: Mon Jan 6 18:52:01 2025 +1100 df31e5ccb8
          </li>
        
      </ul>
    </div>
    <div class="col-md-2">
<a href="https://github.com/seL4/docs/blob/master/Tutorials/hello-camkes-timer.md">View page on GitHub</a>
      <br />
      <a href="https://github.com/seL4/docs/edit/master/Tutorials/hello-camkes-timer.md">Edit page on GitHub</a>
      <br />
      <a href="/sitemap">Sitemap</a>
    </div>

  </div>

</footer>

  </body>
</html>
